VERS5 
NIL 
((DEMORGAN NORMAL#5) (DEMORGAN1 NORMAL#6) (EXCLUDED_MIDDLE NORMAL#7) (TRANS_COND NORMAL#8) (DISJUNCTIVE_SYLLOGISM NORMAL#9) (NORMAL NORMAL#1 NORMAL#2 NORMAL#3 NORMAL#4)) (|∀P Q R.(P∨Q)∧R≡P∧R∨Q∧R| . (AXIOM (TM& . |∀P Q R.(P∨Q)∧R≡P∧R∨Q∧R|)) . ((R . (TRUTHVAL . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . NORMAL#1 . NIL . VARIABLE .)) (Q . (TRUTHVAL . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . NORMAL#1 . NIL . VARIABLE .)) (P . (TRUTHVAL . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . NORMAL#1 . NIL . VARIABLE .))) . NIL . (NORMAL#1) . NIL . NORMAL . NIL . 1 .)(|∀P Q R.R∧(P∨Q)≡R∧P∨R∧Q| . (AXIOM (TM& . |∀P Q R.R∧(P∨Q)≡R∧P∨R∧Q|)) . (R Q P) . NIL . (NORMAL#2) . NIL . NORMAL . NIL . 2 .)(|∀P Q R.R∧(P∨Q)≡P∧R∨Q∧R| . (AXIOM (TM& . |∀P Q R.R∧(P∨Q)≡P∧R∨Q∧R|)) . (R Q P) . NIL . (NORMAL#3) . NIL . NORMAL . NIL . 3 .)(|∀P Q R.(P∨Q⊃R)≡(P⊃R)∧(Q⊃R)| . (AXIOM (TM& . |∀P Q R.(P∨Q⊃R)≡(P⊃R)∧(Q⊃R)|)) . (R Q P) . NIL . (NORMAL#4) . NIL . NORMAL . NIL . 4 .)(|∀P Q.¬(P∨Q)≡¬P∧¬Q| . (AXIOM (TM& . |∀P Q.¬(P∨Q)≡¬P∧¬Q|)) . (R Q P) . NIL . (NORMAL#5) . NIL . NORMAL . NIL . 5 .)(|∀P Q.¬(P∧Q)≡¬P∨¬Q| . (AXIOM (TM& . |∀P Q.¬(P∧Q)≡¬P∨¬Q|)) . (R Q P) . NIL . (NORMAL#6) . NIL . NORMAL . NIL . 6 .)(|∀P Q.P≡(Q⊃P)∧(¬Q⊃P)| . (AXIOM (TM& . |∀P Q.P≡(Q⊃P)∧(¬Q⊃P)|)) . (R Q P) . NIL . (NORMAL#7) . NIL . NORMAL . NIL . 7 .)(|∀P Q R.(Q⊃R)∧(IF P THEN Q ELSE R)⊃R| . (DERIVE (TM& . |∀P Q R.(Q⊃R)∧(IF P THEN Q ELSE R)⊃R|) ((LR&)) NIL) . (R Q P) . NIL . NIL . NIL . NORMAL . NIL . 8 .)(|∀PSI THETA.(∀XW.PSI(XW)⊃THETA(XW))∧(∀XW.¬PSI(XW)⊃THETA(XW))⊃(∀XW.THETA(XW))| . (AXIOM (TM& . |∀PSI THETA.(∀XW.PSI(XW)⊃THETA(XW))∧(∀XW.¬PSI(XW)⊃THETA(XW))⊃(∀XW.THETA(XW))|)) . ((XW . (GROUND . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . NORMAL#9 . NIL . VARIABLE .)) (THETA . (GROUND→TRUTHVAL . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . NORMAL#9 . NIL . VARIABLE .)) (PSI . (GROUND→TRUTHVAL . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . NORMAL#9 . NIL . VARIABLE .))) . NIL . (NORMAL#9) . NIL . NORMAL . NIL . 9 .)